COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.REQUIRE "206MAC.PUB[206,LSP]" source_file
C00003 00003	.hd206 FALL 1979
C00008 ENDMK
C⊗;
.REQUIRE "206MAC.PUB[206,LSP]" source_file;
.
.odd heading(,,{page}) ;
.even heading({page}, , ) ;
.
.LSPFONT
.basicops 
.
.allops
.itemmac 1;
.
.PORTION MAINPORTION
.hd206 FALL 1979
.PAGE ← 1
.hw 2, |Oct. 29|

.begin 
.indent 0,3
.item ← 0

.bb More about append.
#.  Prove the following cancellation rules for ⊗append:  
.begin nofill

##. ∀u v w:[ [u*w=v*w]≡[u=v] ]
##. ∀u v w:[ [w*u=w*v]≡[u=v] ]
.end

.bb Rightwing lists.

#.  Recall that when restricted to lists the operations ⊗car, ⊗cdr and ⊗cons 
behave unsymmetrically.  Thus it is easy to get the first (left most)
element of a list and the rest of the list.   Often one would like to
work on the other end of a list.  

##.  Write programs to compute the functions ⊗rac, ⊗rdc and ⊗snoc, 
where for non-empty lists ⊗uu, ⊗rac[uu] is the last element, ⊗rdc[uu] is 
the list obtained by removing the last element, and for a list ⊗u, 
and an S-expression ⊗x, ⊗snoc[u,x] adds ⊗x to the end of the list ⊗u.  
Use only ⊗car, ⊗cdr, ⊗cons and recursive defintion.

##.  Give axioms characterizing the functions ⊗rac, ⊗rdc and ⊗snoc representing
your programs.

The functions ⊗rac, ⊗rdc, ⊗snoc have the following properties
.begin nofill indent 8,8

  (i)  ⊗rac of a non-empty list is an S-expression,
 (ii)  ⊗rdc of a non-empty list is an list,
(iii)  ⊗snoc of a list and an S-expression is a non-empty list,
 (iv)   the ⊗rac of the ⊗snoc of a list, ⊗u,  and an S-expression, ⊗x, is ⊗x, 
  (v)   the ⊗rdc of the ⊗snoc of a list, ⊗u,  and an S-expression, ⊗x, is ⊗u, and
 (vi)   for a non-empty list ⊗uu, ⊗snoc of the ⊗rdc and the ⊗rac of ⊗uu is just ⊗uu.  
.end

##.  Give domain/range specifications and axioms formallizing the above
properties of ⊗rac, ⊗rdc and ⊗snoc.  

##.  Prove that your programs satisfy these specifications (using the axioms
for the representation of the programs as functions).


.bb Splitting lists.

#.  A pair of lists ⊗⊗[v_._w]⊗ is said to split a list ⊗u (⊗⊗Issplit[v,w,u]⊗)
if ⊗⊗v*w=u⊗.  Write a program ⊗splits[u] that computes a list containing
exactly those pairs of lists that split the list ⊗u.  Give a sentence that
defines the relation ⊗Allsplits[w,u], characterizing 
the list ⊗w of all splits of a list ⊗u and show that your program is
correct with respect to this specification.

.end